T:Type, n:, x:T, L:(T List). (x  nth_tl(n;L))  (x  L) 

latex

ProofTree

Definitions

s = t, t  T, , Type, x:AB(x), type List, (x  l), P  Q, x:A. B(x), {x:A| B(x)} , A  B, i  j , False, A, #$n, -n, n+m, n - m, a < b, Void, i <z j, i z j, , , s ~ t, {T}, SQType(T), [car / cdr], x:A  B(x), P & Q, P  Q, P  Q, ||as||, x:A.B(x), Top, S  T, A List, [], nth_tl(n;as), tl(l), ff, , b, b, True, tt, T, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, [d], p  q, p  q, p q, Unit, left + right, P  Q, x:A. B(x)

Lemmas

cons member, nth tl wf, eqtt to assert, assert of le int, iff transitivity, eqff to assert, iff wf, rev implies wf, true wf, squash wf, bnot of le int, assert of lt int, le int wf, le wf, bool wf, lt int wf, assert wf, bnot wf, length wf nat, member wf, top wf, non neg length, cons one one, guard wf, ge wf, nat properties, l member wf, nat wf, nat ind tp